\begin{tabbing} (\=(((InstConcl [$\parallel$$L_{1}$$\parallel$+$i$]) \+ \\[0ex]CollapseTHEN (Auto'))$\cdot$) \\[0ex]CollapseTHEN ((( \-\\[0ex]R\=WO "select\_append\_back" 0) \+ \\[0ex]CollapseTHEN (((Auto') \\[0ex]CollapseTHEN (((All ArithSimp) \\[0ex] \\[0ex]CollapseTHEN (Auto$\cdot$))$\cdot$))$\cdot$))$\cdot$))$\cdot$ \- \end{tabbing}